T:Type, eq:EqDecider(T), as,bs:(T List), x:T.
(x  l-union(eq; as; bs))  ((x  as)  (x  bs)) 

latex

Definitions	l-union(eq; as; bs), Type, t  T, x:A. B(x), EqDecider(T), type List, False, x:AB(x), P  Q, x:A  B(x), P  Q, P  Q, left + right, P  Q, [], (x  l), P  Q, prop{i:l}, s = t, cons(car; cdr), insert(eq; a; L), guard(T)
Lemmas	member-insert, insert wf, iff functionality wrt iff, or functionality wrt iff, cons member, l-union wf, l member wf, nil member, deq wf